$\forall$$D$:dsys\{i:l\}, $P$:(\{${\it es}$:ES\{i\}$\mid$ d{-}es\{i:l\}($D$; ${\it es}$) \}$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$).
\\[0ex]d{-}realizes2\{i:l\}($D$; ${\it es}$.$P$(${\it es}$)) $\in$ Prop$_{\mbox{\scriptsize i''}}$